\begin{tabbing}
(((((((Auto\_aux (first\_nat 1:n) ((first\_nat 1:n),(first\_nat 3:n)) (first\_tok :t
\\[0ex])\= inil\_term)) \+
\\[0ex]CollapseTHEN (All (Unfolds ``sublist no\_repeats``)))$\cdot$) 
\\[0ex]CollapseTHEN (
\-\\[0ex]A\=ll Reduce))$\cdot$) \+
\\[0ex]CollapseTHEN (ExRepD))$\cdot$
\-
\end{tabbing}